Nuprl Lemma : xxorder_split
13,42
postcript
pdf
T
:Type,
R
:(
T
T
).
order(
T
;
R
)
(
x
,
y
:
T
. Dec(
x
=
y
))
(
a
,
b
:
T
. (
R
(
a
,
b
))
(((
R
\)(
a
,
b
))
(
a
=
b
)))
latex
Up
gen
algebra
1
Definitions of Statement
refl(
T
;
E
)
,
trans(
T
;
E
)
,
anti_sym(
T
;
R
)
,
order(
T
;
R
)
,
E
\
Definitions
anti_sym(
T
;
R
)
,
trans(
T
;
E
)
,
refl(
T
;
E
)
,
E
\
,
order(
T
;
R
)
,
strict_part(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
,
x
(
s1
,
s2
)
,
Order(
T
;
x
,
y
.
R
(
x
;
y
))
Lemmas
order
split
origin
T:Type, R:(T
T
).
(x, y:T. Dec(x = y)) (a, b:T. (R(a,b)) 
(((R\)(a,b)) 
(a = b))) T:Type, R:(TT).
(x, y:T. Dec(x = y)) (a, b:T. (R(a,b)) (((R\)(a,b)) (a = b)))